M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id,
ms:(tg:Idif source(l) = i M.da(rcv(l,tg)) else Top fi) List.
M.send(k;l;s;v;ms;i)  Prop 

latex

Definitions	Unit, P  Q, P & Q, , b, A, concat(ll), map(f;as), f(x), State(ds), 2of(t), x. t(x), f(x)?z, 1of(t), a:A fp B(a), x  dom(f), deq-member(eq;x;L), product-deq(A;B;a;b), KindDeq, IdLnkDeq, a = b, source(l), rcv(l,tg), x:A. B(x), IdLnk, Knd, M.send(k;l;s;v;ms;i), MsgA, M.da(a), M.V(k), M.state, Valtype(da;k), z != f(x)  P(a;z), t  T, P  Q, if b t else f fi, Top, Id, b, Prop
Lemmas	msga wf, Knd wf, IdLnk wf, ma-st wf, ma-v wf, Id wf, top wf, rcv wf, ma-da wf, lsrc wf, eq id wf, ifthenelse wf, idlnk-deq wf, Kind-deq wf, product-deq wf, deq-member wf, assert wf, pi2 wf, fpf-cap wf, pi1 wf, ma-state wf, fpf-ap wf, map wf, concat wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-cap-void-subtype, subtype rel self